$\forall$$a$:Id, $T$, $A$:Type, $x$:Id, $P$:($A$$\rightarrow$$T$$\rightarrow$Prop). ma{-}single{-}pre1($x$;$A$;$a$;$T$;$x$,$v$.$P$($x$,$v$)) $\in$ MsgA